Inference at * 1 
Iof proof for Lemma can-apply-fun-exp-add-iff:



1. A : Type
2. n : 
3. m : 
4. f : A(A + Top)
5. x : A
6. can-apply(f^n+m;x)
  (can-apply(f^m;x)) & (can-apply(f^n;do-apply(f^m;x))) 

latex

 by ((FLemma `can-apply-fun-exp-add` [-1]) 
CollapseTHEN (Auto)) 

latex

C.

Definitions	x:A. B(x), P  Q, {T}, t  T, n+m, x:AB(x), , Type, P & Q, x:A  B(x), can-apply(f;x), do-apply(f;x), f^n, b, s = t
Lemmas	can-apply-fun-exp-add